Termination w.r.t. Q proof of TRS/higher-order/BirdTreeMap.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(treemap, f), app(app(node, x), xs)) → app(app(node, app(f, x)), app(app(map, app(treemap, f)), xs))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(treemap, f), app(app(node, x), xs)) → app(app(node, app(f, x)), app(app(map, app(treemap, f)), xs))

Q is empty.